Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A strict inequality relation or tight apartness relation is an apartness relation which is also a tight relation. An inequality space is a set with a strict inequality relation. Strict inequalities are contrasted with weak inequality or denial inequality, which is the negation of equality. In the context of excluded middle, every weak inequality is a strict inequality relation, so one simply talks about “inequality”.
In set theory, an inequality space is a set with a binary relation such that
In dependent type theory, an inequality space is a type with
where is inductively defined by
The last condition ensures that the type is an h-set.
Given two inequality spaces and , a function is strongly extensional if implies ; that is, reflects apartness. is a strongly injective if is logically equivalent to . The contrapositive of the both conditions imply that preserves equality and is an injection respectively.
Strict inequality is stable if it is logical equivalent to denial inequality; i.e. for all elements and , if and only if . Stable strict inequality is simply called “inequality”, as there is no need to distinguish between strict inequality and denial inequality in this case.
Strict inequality is decidable if for all elements and , or . Decidable strict inequality implies stable strict inequality, so it is usually called decidable inequality. In the context of excluded middle, every strict inequality relation is decidable.
In the category of inequality spaces, monomorphisms between inequality spaces are strongly extensional functions that preserve strict inequality, or strong injections. These monomorphisms are regular monomorphisms. The category of inequality spaces has all (small) limits, created by the forgetful functor to Set. (For example, iff or .) Similarly, it has all finite coproducts. In fact, this category is a complete category. It is not, however, a Grothendieck topos (or even a topos at all), because it doesn't have all infinite coproducts. (To be precise, the statement that it has all small coproducts, or even that it has a subobject classifier, seems to be equivalent to excluded middle.) Nor is it finitely cocomplete, because it does not have all quotients.
We can say, however, that it has coproducts indexed by inequality spaces, although to make this precise is a triviality. More interestingly, it has products indexed by inequality spaces; that is, it is (even locally) a cartesian closed category. In particular, given inequality spaces and , the set of strongly extensional functions from to becomes an inequality space under the rule that iff for some . Finally, the category of inequality spaces has a real numbers object, the Dedekind real numbers.
In classical mathematics, it is true that every set is an inequality space. In constructive mathematics, however, not all sets are inequality spaces. Instead, one can add an axiom to the foundations of mathematics which states that every set is an inequality space.
Axiom of inequality spaces: Every set has a strict inequality relation.
Alternatively, one could take the strict inequality to be foundational, in which the axiom of extensionality becomes
Axiom of extensionality: for any set and , if and only if for all , if and only if .
In dependent type theory, one can make every type into an inequality space by adding the following set of rules to the type theory:
This implies axiom K and uniqueness of identity proofs.
There are also generalisations of the principles of omniscience involving inequality spaces:
Every inequality space has decidable tight apartness, which generalises LPO and analytic LPO
Every inequality space has decidable equality, which generalises WLPO and analytic WLPO
Every inequality space has stable tight apartness, which generalises Markov's principle and analytic Markov's principle
These are all still weaker than excluded middle since in general, the set of truth values is only an inequality space if and only if excluded middle holds.
Since inequality spaces have finite limits, the usual constructions of universal algebra apply; it's straightforward to define inequality groups, inequality rings, and so on.
The various subsets that appear in algebra (such as subgroups, ideals, and cosets) become less fundamental than certain subsets that are, classically, simply their complements. For example, a left ideal in a ring is a subset such that , whenever , and whenever . But a left antiideal in an inequality ring is an -open subset such that is false, or whenever , and whenever . (The -openness requirement is automatic if is strengthened to for all , using that the ring operations are strongly extensional.) Note that the complement of an antiideal is an ideal, but not every ideal can be constructively shown to be the complement of an antiideal; so antiideals are more fundamental than ideals, in an inequality ring.
Prime ideals are even more interesting. A two-sided antiideal (so also satisfying that whenever ) is antiprime (or simply prime if no confusion is expected) if and whenever . Now the complement of an antiprime antiideal may not be a prime ideal (as normally defined). But in fact, it is antiprime antiideals that are more important in constructive algebra. In particular, an integral domain in constructive algebra is an inequality ring in which the antiideal of nonzero elements is antiprime.
Any apartness relation on an inequality space is the same as the (strongly) closed equivalence relation on the discrete locale . This localic perspective on apartness relations extends naturally to anti-algebra: an antiideal is the same as a closed ideal in a discrete localic ring that respects the closed equivalence relation corresponding to . Equivalently, this is a closed ideal of the -topology regarded as a (non-discrete) localic ring. The spatial part of this closed localic ideal is then the ordinary ideal complementary to the antiideal, and so on. Moreover, since unions of closed sublocales correspond to intersections of their open complements, an antiideal is antiprime exactly when its corresponding closed localic ideal is “prime” in an appropriate internal sense in Loc, namely that , where is the multiplication. The fact that the complement of an antiprime antiideal need not be prime in the usual sense corresponds to the fact that taking the spatial part of sublocales doesn’t commute with unions.
For more about apartness algebra, see antisubalgebra.
Last revised on September 5, 2024 at 16:47:10. See the history of this page for a list of all contributions to it.